package Services;

import Impl.Type;

public interface TerrainService {
	// INVARIANTS
	// inv: getNbJoueur()==1
	
	// inv: 1<=getXJoueur()<=getSizeX()
	// inv: 1<=getYJoueur()<=getSizeY()
	// inv: getNbPorte()==1 || !isStarted()
	// inv: getNbDiamant()>=0
	
	// min: getTypeBloc(x,y)=BlocService::getType(getBloc(x,y))
	// min: getOldTypeBloc(x,y)=BlocService::getOldType(getBloc(x,y))
	
	
	// CONSTRUCTEURS
	// pre: init(x, y) require x>1 && y>1
	// post: getBloc(1,1) == BlocService::init(Type.Hero)
	// post: forall x in [1,getSizeX()], y in [1,getSizeY()] with (!(x==1 && y==1)) -> getBloc(x, y)==BlocService::init(Type.Vide)
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==false
	// post: getXJoueur()==1
	// post: getYJoueur()==1
	// post: getNbJoueur()==1
	// post: getNbDiamant()==0
	// post: getNbPorte()==0
	// post: getSizeX()==sizeX
	// post: getSizeY()==sizeY
	// post: isStarted()==false
	public void init(int sizeX, int sizeY);
	public void init(String filename);
	// post: forall x in [1,getSizeX()], y in [1,getSizeY()]  -> getBloc(x, y).equals(getBloc(terrain, x, y))
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==isChanged(terrain, x, y)
	// post: getXJoueur()==getXJoueur(terrain)
	// post: getYJoueur()==getYJoueur(terrain)
	// post: getNbJoueur()==getNbJoueur(terrain)
	// post: getNbDiamant()==getNbDiamant(terrain)
	// post: getNbPorte()==getNbPorte(terrain)
	// post: getSizeX()==getSizeX(terrain)
	// post: getSizeY()==getSizeY(terrain)
	// post: isStarted()==TerrainService::isStarted(terrain)
	public void clone(TerrainService terrain);
	
	// OBSERVATEURS
	/*const*/ public int getSizeX();
	/*const*/ public int getSizeY();
	
	public BlocService getBloc(int x, int y);
	public Type getTypeBloc(int x, int y);
	public Type getOldTypeBloc(int x, int y);
	
	public int getXJoueur();
	public int getYJoueur();
	
	public int getNbDiamant();
	public int getNbPorte();
	public int getNbJoueur();
	
	public boolean isChanged(int x, int y);
	
	public boolean isStarted();
	
	
	// OPERATEURS
	// pre : startTerrain() require !isStarted() && getNbPorte()==1 && getNbDiamant>0
	// post: getXJoueur()==getXJoueur()@pre
	// post: getYJoueur()==getYJoueur()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: getNbDiamant()==getNbDiamant()@pre
	// post: getNbPorte()==getNbPorte()@pre
	// post: isStarted()==true
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==isChanged(x,y)@pre
	// post: forall a in [1,getSizeX()], b in [1, getSizeY()] -> getBloc(a,b).equals(getBloc(a,b)@pre)
	public void startTerrain();
	
	// pre : addObject(x, y, type) require !isStarted() && 1<=x<=getSizeX() && 1<=y<=getSizeY() 
	//							&& type notin {Hero,SortieOuverte} && getTypeBloc(x,y)==Type.Vide
	// post: getXJoueur()==getXJoueur()@pre
	// post: getYJoueur()==getYJoueur()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: if(type==Type.Diamant)
	//			getNbDiamant()==getNbDiamant()@pre+1
	//		 else getNbDiamant()==getNbDiamant()@pre
	// post: if(type==Type.SortieFermee)
	//			getNbPorte()==getNbPorte()@pre+1
	//		 else getNbPorte()==getNbPorte()@pre
	// post: isStarted()==isStarted()@pre
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==isChanged(x,y)@pre
	// post: BlocService tmp = getBloc(x,y)
	// 		 forall a in [1,getSizeX()], b in [1, getSizeY()] -> 
	//			if(getBloc(a,b)==tmp)
	//				getBloc(a,b)==BlocService::changeType(getBloc(a,b),type)
	//			else
	//				getBloc(a,b)==getBloc(a,b)@pre
	public void addObject(int x, int y, Type type);
	
	
	// pre: openDoor() require isStarted() && getNbDiamant==0
	// post: forall a in [1,getSizeX()], b in [1, getSizeY()] -> 
	//			if(getTypeBloc(a,b)@pre!=Type.SortieFermee)
	//				 getBloc(a,b).equals(getBloc(a,b)@pre)
	//			else
	//				getBloc(a,b)==BlocService::changeType(getBloc(a,b)@pre, Type.SortieOuverte)
	// post: getXJoueur()==getXJoueur()@pre
	// post: getYJoueur()==getYJoueur()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: getNbDiamant()==getNbDiamant()@pre
	// post: getNbPorte()==getNbPorte()@pre	
	// post: isStarted()==isStarted()@pre
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==isChanged(x,y)@pre
	public void openDoor();
	
	// pre: validate() require isStarted()
	// post: getXJoueur()==getXJoueur()@pre
	// post: getYJoueur()==getYJoueur()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: getNbDiamant()==getNbDiamant()@pre
	// post: getNbPorte()==getNbPorte()@pre
	// post: isStarted()==isStarted()@pre
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==false
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> getBloc(x,y).equals(getBloc(x,y)@pre)
	public void validate();

	
	// pre: moveObject(x,y,xnew,ynew) require getTypeBloc(x,y) C {Rocher, Diamant}
	// pre: moveObject(x,y,xnew,ynew) require getTypeBloc(xnew,ynew) C {Hero, Vide}
	// pre: moveObject(x,y,xnew,ynew) require !isChanged(x,y)
	// pre: moveObject(x,y,xnew,ynew) require isStarted()
	// post: getXJoueur()==getXJoueur()@pre
	// post: getYJoueur()==getYJoueur()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: getNbDiamant()==getNbDiamant()@pre
	// post: getNbPorte()==getNbPorte()@pre
	// post: isStarted()==isStarted()@pre
	// post: isChanged(xnew, ynew)==true
	// post:
	//		BlocService bloc = getBloc(xnew, ynew)
	//		forall a in [1,getSizeX()], b in [1, getSizeY()] with!(getBloc(a,b)!=bloc)->  
	//				isChanged(a, b)==isChanged(a,b)@pre
	// post: 
	//		BlocService blocNew = getBloc(xnew, ynew)
	//		BlocService bloc = getBloc(x, y)
	//		forall a in [1,getSizeX()], b in [1, getSizeY()] -> 
	//  		if(getBloc(a,b)==bloc)
	//				getBloc(a,b)==BlocService::changeType(getBloc(a,b)@pre, Type.Vide)
	// 			else if(getBloc(a,b)==blocNew)
	//				getBloc(a,b)==BlocService::changeType(getBloc(a,b)@pre, getTypeBloc(x,y)@pre)
	//			else
	//				getBloc(a,b).equals(getBloc(a,b)@pre)
	public void moveObject(int x, int y, int xnew, int ynew);
	

	// pre: putHero(x,y) require 0<=x<=getSizeX()+1 && 0<=y<=getSizeY()+1
	// post: isStarted()==isStarted()@pre
	// post: getNbJoueur()==getNbJoueur()@pre
	// post: getNbPorte()==getNbPorte()@pre 
	// post: if(x==0)getXJoueur()==getSizeX()
	//		 else if(x==getSizeX()+1) getXJoueur()==1
	//		 else getXJoueur()==x
	// post: if(y==0)getYJoueur()==getSizeY()
	//		 else if(y==getSizeY()+1) getYJoueur()==1
	//		 else getYJoueur()==y
	// post: if(getTypeBloc(x,y)@pre == Type.Diamant)
	//			getNbDiamant()==getNbDiamant()@pre-1
	//		 else getNbDiamant()==getNbDiamant()@pre
	// post: forall x in [1,getSizeX()], y in [1, getSizeY()] -> isChanged(x,y)==isChanged(x,y)@pre
	// post: forall a in [1,getSizeX()], b in [1, getSizeY()] -> 
	//		if(a==x && b==y)
	//			getBloc(a,b)==BlocService::changeType(getBloc(a,b)@pre, Type.Hero)
	//		else if(a==getXJoueur()@pre && b==getYJoueur()@pre)
	//			getBloc(a,b)==BlocService::changeType(getBloc(a,b)@pre, Type.Vide)
	//		else
	//			getBloc(a,b).equals(getBloc(a,b)@pre)
	public void putHero(int x, int y);

}
